|
1: |
|
if(true,x,y) |
→ x |
2: |
|
if(false,x,y) |
→ y |
3: |
|
eq(0,0) |
→ true |
4: |
|
eq(0,s(x)) |
→ false |
5: |
|
eq(s(x),0) |
→ false |
6: |
|
eq(s(x),s(y)) |
→ eq(x,y) |
7: |
|
app(nil,l) |
→ l |
8: |
|
app(cons(x,l1),l2) |
→ cons(x,app(l1,l2)) |
9: |
|
app(app(l1,l2),l3) |
→ app(l1,app(l2,l3)) |
10: |
|
mem(x,nil) |
→ false |
11: |
|
mem(x,cons(y,l)) |
→ ifmem(eq(x,y),x,l) |
12: |
|
ifmem(true,x,l) |
→ true |
13: |
|
ifmem(false,x,l) |
→ mem(x,l) |
14: |
|
inter(x,nil) |
→ nil |
15: |
|
inter(nil,x) |
→ nil |
16: |
|
inter(app(l1,l2),l3) |
→ app(inter(l1,l3),inter(l2,l3)) |
17: |
|
inter(l1,app(l2,l3)) |
→ app(inter(l1,l2),inter(l1,l3)) |
18: |
|
inter(cons(x,l1),l2) |
→ ifinter(mem(x,l2),x,l1,l2) |
19: |
|
inter(l1,cons(x,l2)) |
→ ifinter(mem(x,l1),x,l2,l1) |
20: |
|
ifinter(true,x,l1,l2) |
→ cons(x,inter(l1,l2)) |
21: |
|
ifinter(false,x,l1,l2) |
→ inter(l1,l2) |
|
There are 19 dependency pairs:
|
22: |
|
EQ(s(x),s(y)) |
→ EQ(x,y) |
23: |
|
APP(cons(x,l1),l2) |
→ APP(l1,l2) |
24: |
|
APP(app(l1,l2),l3) |
→ APP(l1,app(l2,l3)) |
25: |
|
APP(app(l1,l2),l3) |
→ APP(l2,l3) |
26: |
|
MEM(x,cons(y,l)) |
→ IFMEM(eq(x,y),x,l) |
27: |
|
MEM(x,cons(y,l)) |
→ EQ(x,y) |
28: |
|
IFMEM(false,x,l) |
→ MEM(x,l) |
29: |
|
INTER(app(l1,l2),l3) |
→ APP(inter(l1,l3),inter(l2,l3)) |
30: |
|
INTER(app(l1,l2),l3) |
→ INTER(l1,l3) |
31: |
|
INTER(app(l1,l2),l3) |
→ INTER(l2,l3) |
32: |
|
INTER(l1,app(l2,l3)) |
→ APP(inter(l1,l2),inter(l1,l3)) |
33: |
|
INTER(l1,app(l2,l3)) |
→ INTER(l1,l2) |
34: |
|
INTER(l1,app(l2,l3)) |
→ INTER(l1,l3) |
35: |
|
INTER(cons(x,l1),l2) |
→ IFINTER(mem(x,l2),x,l1,l2) |
36: |
|
INTER(cons(x,l1),l2) |
→ MEM(x,l2) |
37: |
|
INTER(l1,cons(x,l2)) |
→ IFINTER(mem(x,l1),x,l2,l1) |
38: |
|
INTER(l1,cons(x,l2)) |
→ MEM(x,l1) |
39: |
|
IFINTER(true,x,l1,l2) |
→ INTER(l1,l2) |
40: |
|
IFINTER(false,x,l1,l2) |
→ INTER(l1,l2) |
|
The approximated dependency graph contains 4 SCCs:
{23-25},
{22},
{26,28}
and {30,31,33-35,37,39,40}.